COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	ANOTHER NOTE ON THE CHECKERBOARD PROBLEM
C00004 ENDMK
C⊗;
ANOTHER NOTE ON THE CHECKERBOARD PROBLEM


	In 1964, wrote a Stanford Artificial Intelligence Memo entitled
A Tough Nut for Theorem Provers.  The intent of this note was to give a
theorem that I didn't think current theorem proving programs were likely
to be able prove.  Indeed, although the theorem was a sentence of first
order logic, it seemed to me that there might not be any reasonably short
proof of it within first order logic.

	The problem is the following:  An eight by eight checker board
has two diagonally opposite squares removed - say the lower left and
the upper right squares.  The problem - a well known puzzle - is to determine
whether it is possible to cover this mutilated board with dominoes, each
dominoe covering two horizontally or vertically adjacent squares.

	The well known proof that the covering is impossible consists in
noting that each dominoe covers one square of each color, and therefore
any covering by dominoes covers equal numbers of squares of each color.
However, since the two removed squares are of the same color, there are
32 squares of one color and 30 of the other to be covered, and so the
covering is impossible.